M:MsgA, a:Id. a in dom(M.pre)  Prop 

latex

Definitions	MsgA, a in dom(M.pre), b, x  dom(f), IdDeq, a:A fp B(a), x. t(x), State(ds), Valtype(da;k), locl(a), x:A. B(x), Prop, t  T, Id
Lemmas	Id wf, locl wf, ma-valtype wf, ma-state wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert wf, msga wf